$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($x$:$A$ $\times$ $B$($x$)), $C$:Type, $b$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$$C$).
\\[0ex]let $x$,$y$ = $p$ in $b$($x$,$y$) = $b$($p$.1,$p$.2)